/*

Indice:

1	UTENTI:
			1.1	definizioni
			1.2	fatti
			1.3 	predicato show (statico)
			1.4	predicati operazioni (dinamici)
			1.5	asserzioni

2	PRODOTTI BASE
			2.1	definizioni
			2.2	fatti
			2.3 	predicato show (statico)
			2.4	predicati operazioni (dinamici)
			2.5	asserzioni

3	PACCHETTI
			3.1	definizioni
			3.2	fatti
			3.3 	predicato show (statico)
			3.4	predicati operazioni (dinamici)
			3.5	asserzioni

4 show

*/


//----------------------------------1 UTENTI
//----------------------------------1.1	UTENTI DEFINIZIONI


sig Email {}
sig Stringa {}

abstract sig Utente {
	username: Stringa,
	password: Stringa,
	userEmail: Email
	// per semplicità si omettono gli altri attributi dell'entità Utente
}

sig Cliente extends Utente {
	listaAcquisti: set PacchettoPrivato,
	pacchettoInCostruzione: lone PacchettoPrivato
}

sig TravelAgent extends Utente {}

one sig Amministratore extends Utente {}

sig DBUtenti {
	dipendenti: set TravelAgent,							//insieme dei dipendenti che lavorano per l'agenzia
	admin: Amministratore,
	registra: Amministratore -> set TravelAgent,	//dipendenti registrati nel sistema
	clientiRegistrati: set Cliente							//clienti registrati nel sistema
}


//----------------------------------1.2	UTENTI FATTI


fact utentiNelDB{
	//tutti gli utenti sono presenti in qualche DB
	all c:Cliente | some u:DBUtenti | c in u.clientiRegistrati
	all t:TravelAgent | some u:DBUtenti | t in u.dipendenti 

	//tutti i dipendenti dell'agenzia vengono registrati nel sistema dall'amministratore
	all t:TravelAgent, u:DBUtenti | t in u.dipendenti iff t in Amministratore.(u.registra)
}


fact VincoliDatiPersonali {
	//username e password sono esclusivi per ogni utente
	no disj u1,u2:Utente | u1.username = u2.username
	no disj u1,u2:Utente | u1.userEmail = u2.userEmail
}


//----------------------------------1.3	UTENTI PREDICATO SHOW


//predicato per visualizzare le possibili configurazioni degli utenti nel sistema
pred showUtenti {
	//utilità per visualizzare meglio le istanze
	#CatalogoProdotti = 0
	#ProdottoBase = 0
	#CatalogoPacchetti = 0
	#PacchettoViaggio = 0
	#Località = 0
	#DBUtenti = 1
	all s:Stringa | some u:Utente | s = u.username
	all e:Email | some u:Utente | e = u.userEmail
}run showUtenti for 6


//----------------------------------1.4	UTENTI PREDICATI OPERAZIONI


pred assumiERegistraTravelAgent[u1,u2:DBUtenti, t:TravelAgent, n,p:Stringa, e:Email]{
	u1 != u2
	t not in u1.dipendenti										//arriva un nuovo dipendente
	u2.dipendenti = u1.dipendenti + t						//assumo il dipendente
	u2.registra = u1.registra + Amministratore->t	//l'amministratore lo registra nel sistema
	t.username = n													//definendone i dati personali
	t.password = p
	t.userEmail = e
	u2.clientiRegistrati = u1.clientiRegistrati			//mantengo invariate le altre registrazioni

	//utilità per visualizzare meglio le istanze
	#CatalogoProdotti = 0
	#ProdottoBase = 0
	#CatalogoPacchetti = 0
	#PacchettoViaggio = 0
	#Località = 0
	#DBUtenti = 2
}run assumiERegistraTravelAgent for 4


//----------------------------------1.5	UTENTI ASSERZIONI


assumiDipendenteNonRegistrato: check {
	//un dipendente non può già essere registrato nel sistema prima della sua assunzione
	all u1,u2:DBUtenti, t:TravelAgent, n,p:Stringa , e:Email | assumiERegistraTravelAgent[u1,u2,t,n,p,e] implies t not in Amministratore.(u1.registra)

	//OSSERVAZIONI:
	//il predicato assumiERegistraTravelAgent controlla solo che il nuovo dipendente non sia già assunto (t not in u1.dipendenti)
	//deriva dai fatti :	1) tutti i dipendenti assunti vengono registrati
	//							2) t è un nuovo dipendente
} for 4


//----------------------------------2 PRODOTTI BASE
//----------------------------------2.1	PRODOTTI BASE DEFINIZIONI


sig Località {}

abstract sig ProdottoBase {
	localitàProdotto: Località
}

abstract sig Trasporto extends ProdottoBase {
	codice: Stringa,
	localitàPartenza: Località,
	localitàArrivo: Località,
	tipologia: String,
	trasportoAssociato: Trasporto		//il trasporto che assicura al clientedi poter tornare alla località di partenza
}{
	localitàPartenza != localitàArrivo	//un trasporto non può partire e arrivare dalla stessa località
	localitàProdotto = localitàArrivo		//per convenzione un trasporto sarà associato alla sua località di destinazione
}

sig Volo extends Trasporto {
}{
	tipologia = "Volo"
}

sig Hotel extends ProdottoBase {
	nomeHotel: Stringa
}

sig Escursione extends ProdottoBase {
	nomeEscursione: Stringa
}

sig CatalogoProdotti {
	inserisceProdotto: TravelAgent -> set ProdottoBase
}


//----------------------------------2.2	PRODOTTI BASE FATTI


fact prodottiNelCatalogo {
	//un prodotto è stato inserito in qualche catalogo da 1 solo dipendente
	all p:ProdottoBase | some c:CatalogoProdotti | one t:TravelAgent | p in t.(c.inserisceProdotto)
	//OSSERVAZIONI
	//'some' usato invece di 'one' per i mondi che necessitano due cataloghi per simulare un'operazione
}


fact VincoliTrasportiELocalità {
	//per ogni trasporto di andata ne esiste almeno uno di ritorno (quello creato dalla procedura 'aggiungiTrasporto')
	all t1:Trasporto, t2:t1.trasportoAssociato | t1.localitàPartenza = t2.localitàArrivo && t1.localitàArrivo = t2.localitàPartenza && t2.trasportoAssociato = t1
}


//----------------------------------2.3	PRODOTTI BASE PREDICATO SHOW


//predicato per visualizzare le possibili configurazioni dei prodotti base nel sistema
pred showProdotti {
	//utilità per visualizzare meglio le istanze
	#DBUtenti = 1
	#Cliente = 0
	#TravelAgent > 1
	#CatalogoProdotti = 1
	#ProdottoBase > 1
	#Hotel < 4
	#CatalogoPacchetti = 0
}run showProdotti for 6


//----------------------------------2.4	PRODOTTI BASE PREDICATI OPERAZIONI


pred aggiungiHotelOEscursione[c1,c2:CatalogoProdotti, t:TravelAgent, l:Località, p:ProdottoBase]{
	//c2 rappresenta il catalogo prodotti c1 dopo l'aggiunta del prodotto p
	c1 != c2
	p in (Hotel + Escursione)												//il prodotto da aggiungere è un hotel o un'escursione
	p.localitàProdotto = l														//il TravelAgent seleziona la località in cui usare il prodotto
	p not in TravelAgent.(c1.inserisceProdotto)					//non è inserito già nel sistema un prodotto uguale
	c2.inserisceProdotto = c1.inserisceProdotto + t->p			//registro quale TravelAgent ha effettuato l'operazione

	//utilità per visualizzare meglio le istanze
	#DBUtenti = 1
	#Cliente = 0
	#TravelAgent > 1
	#CatalogoProdotti = 2
	#Trasporto = 0
	#Hotel = 2
	#Escursione = 1
	#CatalogoPacchetti = 0
	#PacchettoViaggio = 0
}run aggiungiHotelOEscursione for 5


//date due località e un tipo di trasporti il predicato permette ad un Travel Agent di aggiungere al catalogo prodotti una coppia di trasporti che colleghino le località
pred aggiungiTrasporto[c1,c2:CatalogoProdotti, t:TravelAgent, l1,l2:Località, p1:ProdottoBase, type:String]{
	//c2 rappresenta il catalogo prodotti c1 dopo l'aggiunta dei trasporti
	//l1 è la località di partenza del trasporto p1
	//l2 è la località di arrivo del trasporto p1
	//type è la tipologia dei trasporti creati (per ora esiste solo "Volo")
	c1 != c2
	p1 in Trasporto																				//i prodotti da aggiungere sono trasporti

	p1.localitàPartenza = l1																	//caratteristiche del trasporto di andata
	p1.localitàArrivo = l2
	p1.tipologia = type
	p1 not in TravelAgent.(c1.inserisceProdotto)
	
	let p2 = p1.trasportoAssociato {													//p2 è il trasporto creato automaticamente per essere utilizzato con p1	
		p2 not in TravelAgent.(c1.inserisceProdotto)
		p2.tipologia = p1.tipologia
		c2.inserisceProdotto = c1.inserisceProdotto + t->p1 + t->p2		//registro quale Travel Agent ha inserito i prodotti
	}

	//utilità per visualizzare meglio le istanze
	#DBUtenti = 1
	#Cliente = 0
	#TravelAgent > 1
	#CatalogoProdotti = 2
	#Trasporto = 2
	#Hotel = 0
	#Escursione = 0
	#CatalogoPacchetti = 0
}run aggiungiTrasporto for 4


//----------------------------------2.5	PRODOTTI BASE ASSERZIONI


localitàNecessarie: check {
	//se non esistono località nel database allora non è possibile creare prodotti o pacchetti
	#Località = 0 implies #ProdottoBase = 0 && #PacchettoViaggio = 0

	//OSSERVAZIONI:
	//negli use case del Travel Agent del documento di specifica è stata aggiunta un'eccezione sulla creazione precedente di almeno una località
	//è permessa invece la situazione in cui siano state create delle località (antecedente falso) a cui non è ancora associato alcun prodotto (conseguente falso)
} for 4

localitàTrasporti: check {
	//finchè i TravelAgent non hanno inserito nel sistema almeno 2 località non possono creare trasporti
	#Località < 2 implies #Trasporto = 0

	//OSSERVAZIONI:
	//deriva dai fatti: 	1) ogni trasporto ha bisogno di 2 località (una per l'andata e una per il ritorno)
	//							2) le località devono essere diverse
}for 4

presenzaTravelAgent: check {
	//solo i Travel Agent possono inserire prodotti
	#TravelAgent = 0 implies #ProdottoBase = 0

	//OSSERVAZIONI:
	//se #TravelAgent > 0 (antecedente falso) è possibile sia che il database sia vuoto (conseguente vero) sia che qualche prodotto è stato già creato (conseguente falso)
	//non è esplicitato nel conseguente #PacchettiViaggio = 0 poichè senza prodotti non è già possibile costruire un pacchetto	
} for 4


//----------------------------------3 PACCHETTI
//----------------------------------3.1	PACCHETTI DEFINIZIONI


abstract sig PacchettoViaggio {
	idPacchetto: Stringa,
	localitàPacchetto: Località,
	hotelPacchetto: Hotel,
	//a differenza delle specifiche e dell'implementazione qui si considera che un pacchetto possa contenere
	// un set di Escursioni invece che al massimo 1 per rendere più realistico il modello
	escursioniPacchetto: set Escursione	
}

sig PacchettoPubblico extends PacchettoViaggio {}

sig PacchettoPrivato extends PacchettoViaggio {
	trasportoAndata: Trasporto,
	trasportoRitorno: Trasporto,
	dataPartenza: Int,
	dataRitorno: Int,
	numeroPersone: Int
}{
	dataPartenza < dataRitorno
}

sig CatalogoPacchetti {
	inseriscePacchetto: TravelAgent -> set PacchettoPubblico
}


//----------------------------------3.2	PACCHETTI FATTI


fact VincoliPacchetti {
	//ogni pacchetto deve essere utilizzato in 1 determinata località, la stessa in cui: è situato l'hotel e si svolgono le escursioni
	all h:Hotel, p:PacchettoViaggio | h = p.hotelPacchetto implies  h.localitàProdotto = p.localitàPacchetto
	all e:Escursione, p:PacchettoViaggio | e in p.escursioniPacchetto implies  e.localitàProdotto =p.localitàPacchetto
}


fact VincoliPacchettiPubblici {
	//ogni pacchetto pubblico deve essere in un catalogo
	all p:PacchettoPubblico | some c:CatalogoPacchetti | one t:TravelAgent | p in t.(c.inseriscePacchetto)

	//ogni pacchetto pubblico deve differire dagli altri per almeno una sua componente
	//il predicato stessiProdotti è definito poco più avanti
	no disj p1,p2:PacchettoPubblico | stessiProdotti[p1,p2]
}


fact VincoliPacchettiPrivati {
	//in ogni pacchetto privato oltre all'hotel ed escursioni, anche il trasporto di andata deve avere come destinazione il luogo del soggiorno
	all t:Trasporto, p:PacchettoPrivato | t = p.trasportoAndata  implies  t.localitàProdotto = p.localitàPacchetto

	//il trasporto di ritorno deve partire dalla località in cui è arrivato il trasporto di andata
	all p:PacchettoPrivato | p.trasportoAndata.localitàArrivo =  p.trasportoRitorno.localitàPartenza

	//un pacchetto privato esiste solo nella storia degli acquisti del cliente o è il pacchetto che sta personalizzando al momento
	all p:PacchettoPrivato | some c:Cliente | p in c.listaAcquisti || p = c.pacchettoInCostruzione

	//un determinato paccheto privato che si sta creando ora non può essere già stato acquistato in passato
	//non si esclude che ne esista però un altro con le stesse componenti acquistato in passato
	no p:PacchettoPrivato, c:Cliente | p in c.listaAcquisti && p = c.pacchettoInCostruzione

	//un pacchetto privato non può appartenere a più clienti
	//non si esclude che più clienti diversi costruiscano pacchetti con componenti simili ma non saranno lo stesso pacchetto privato
	no p:PacchettoPrivato, c1,c2:Cliente | c1 !=c2 && (p in c1.listaAcquisti || p = c1.pacchettoInCostruzione) && (p in c2.listaAcquisti || p = c2.pacchettoInCostruzione)

	//un pacchetto privato deve derivare dalla personalizzazione di un pacchetto pubblico di cui non si può cambiare la località
	all pr:PacchettoPrivato | some c:CatalogoPacchetti | some pu:TravelAgent.(c.inseriscePacchetto) | pu.localitàPacchetto = pr.localitàPacchetto
}


//----------------------------------3.3	PACCHETTI PREDICATO SHOW


//predicato per visualizzare le possibili configurazioni dei pacchetti nel sistema
pred showPacchetti{
	//utilità per visualizzare meglio le istanze
	#DBUtenti = 1
	#CatalogoProdotti = 1
	#CatalogoPacchetti = 1
	#PacchettoViaggio > 0
}run showPacchetti for 5


//----------------------------------3.4	PACCHETTI PREDICATI OPERAZIONI


pred stessiProdotti[p1,p2:PacchettoViaggio] {
	p1.hotelPacchetto = p2.hotelPacchetto && p1.escursioniPacchetto = p2.escursioniPacchetto
}


pred aggiungiPacchettoPubblico[c1,c2:CatalogoPacchetti, t:TravelAgent, p:PacchettoPubblico, h:Hotel, e:Escursione, l:Località]{
	c1 != c2
	p.localitàPacchetto = l													//il TravelAgent seleziona la località in cui usare il pacchetto
	p not in TravelAgent.(c1.inseriscePacchetto)					//il pacchetto non è inserito già nel sistema
	c2.inseriscePacchetto = c1.inseriscePacchetto+ t->p		//registro quale TravelAgent ha effettuato l'operazione

	//utilità per visualizzare meglio le istanze
	#DBUtenti = 1
	#Cliente = 0
	#CatalogoProdotti = 1
	#CatalogoPacchetti = 2
	#PacchettoPrivato = 0
}run aggiungiPacchettoPubblico for 4


pred aggiungiEscursioneAPacchettoPubblico[c1,c2:CatalogoPacchetti,p1,p2:PacchettoPubblico, e:Escursione, t:TravelAgent]{
	c1 != c2
	p1 != p2
	e not in p1.escursioniPacchetto												//si può aggiungere un'escursione non già presente nel pacchetto
	p1 in TravelAgent.(c1.inseriscePacchetto)								//l'escursione si aggiunge ad un pacchetto già esistente
	p2.escursioniPacchetto = p1.escursioniPacchetto + e				//aggiungo l'escursione e mantengo inalterati gli altri prodotti
	p2.hotelPacchetto = p1.hotelPacchetto

	let eccezione = p2 in TravelAgent.(c1.inseriscePacchetto) {
		! eccezione implies c2.inseriscePacchetto	= c1.inseriscePacchetto - t->p1 + t->p2
												//se l'operazione non porta ad ottenere un pacchetto già presente allora la porto a termine eliminando il pacchetto senza l'escursione e aggiungendo quello nuovo che la contiene	
		eccezione implies c2.inseriscePacchetto = c1.inseriscePacchetto	
												//se l'operazione porta ad ottenere un pacchetto già esistente non tolgo o aggiungo alcun pacchetto
	}
	p2 in TravelAgent.(c1.inseriscePacchetto)		//controllo del flag eccezione
																		// alternativa: p2 not in TravelAgent.(c1.inseriscePacchetto)

	//utilità per visualizzare meglio le istanze
	#DBUtenti = 1
	#CatalogoProdotti = 1
	#CatalogoPacchetti = 2
	#PacchettoViaggio = 2
	#Escursione = 1
//	some p:PacchettoPubblico | #(p.escursioniPacchetto)>2	//per visualizzare il caso in cui si aggiunge un'escursione ad un pacchetto che ne contiene già almeno una
}run aggiungiEscursioneAPacchettoPubblico for 6


presenzaClienti: check {
	//solo i clienti possono creare pacchetti privati
	#Cliente = 0 implies #PacchettoPrivato = 0

	//OSSERVAZIONI:
	//se #Clienti > 0 (antecedente falso) è possibile sia che questi non abbiano fatto acquisti (conseguente vero) sia che qualche pacchetto è stato personalizzato (conseguente falso)
	//deriva dal fatto: tutti  i pacchetti privati sono nella lista acquisti di qualche cliente oppure sono in fase di personalizzazione (da parte di un cliente)
}for 4


//----------------------------------3.5	PACCHETTI ASSERZIONI


condizioniPersonalizzazionePacchetti: check {
		//se non ci sono almeno 2 località e 3 prodotti base non è possibile personalizzare una pacchetto privato
		#Località < 2 || #ProdottoBase < 3 implies #PacchettoPrivato = 0
		
		//OSSERVAZIONI
		//deriva dai fatti: 	1) come già verificato in precedenza per creare 2 trasporti servono minimo 2 località
		//							2) un pacchetto privato necessita dei 2 trasporti
		//							3) a questi deve essere aggiunto 1 hotel e solo opzionalmente alcune escursioni
}for 4


coerenzaLocalitàPacchettoPrivato: check{
	//il viaggio ritorno deve iniziare dalla località in cui si è svolta la vacanza
	all p:PacchettoPrivato | p.trasportoRitorno.localitàPartenza = p.localitàPacchetto

	//OSSERVAZIONI:
	//deriva dai fatti: 	1) il viaggio di ritorno ha la stessa parteza della destinazione del viaggio di andata
	//							2) il viaggio di partenza deve portare alla località della vacanza
}for 4


coerenzaLocalitàAggiungiEscursioneAPacchetto: check {
	//si può aggiungere un'escursione ad un pacchetto solo se si svolge nella stessa località prevista per il viaggio
	all c1,c2:CatalogoPacchetti,p1,p2:PacchettoPubblico, e:Escursione, t:TravelAgent | aggiungiEscursioneAPacchettoPubblico[c1, c2, p1, p2, e, t] implies e.localitàProdotto = p1.localitàPacchetto && e.localitàProdotto = p2.localitàPacchetto
	
	//OSSERVAZIONI:
	//deriva dal fatto:	tutti i componenti di un pacchetto hanno la stessa località di riferimento
}for 4


//----------------------------------4 SHOW

pred show () {
	//utilità per visualizzare meglio le istanze
	#DBUtenti = 1
	#CatalogoProdotti = 1
	#CatalogoPacchetti = 1
}
run show for 5
